(declare-fun _substvar_95_ () Bool)
(declare-fun _substvar_122_ () Int)
(declare-fun _substvar_56_ () Bool)
(declare-const v8 Bool)
(declare-const v14 Bool)
(declare-const v19 Bool)
(declare-const i3 Int)
(declare-const i4 Int)
(declare-const i8 Int)
(declare-const i13 Int)
(declare-const i14 Int)
(push)
(declare-const v35 Bool)
(declare-const v36 Bool)
(declare-const v38 Bool)
(declare-const v50 Bool)
(assert _substvar_56_)
(assert (or v8 v8 (<= i14 i3)))
(assert _substvar_95_)
(assert (or v50 (not v36) v19))
(assert (or v14 (<= i14 i3) v14))
(assert (or (<= 0 i14 _substvar_122_ (abs i8)) v38 (distinct 40 (* (+ i13 81 (div i4 23) 64 64) 40 (div i4 23) (+ i13 81 (div i4 23) 64 64)))))
(assert (or (<= i14 i3) v19 v35))
(check-sat)
